Up	fun 1, fun 1
Wellformedness Lemmas	tidentity wf, tidentity wf for mon hom, tidentity wf
Definitions	Id
FDL editor aliases	tidentity